(DEFUN REDUCE1 (E) 
       (COND ((ATOM E) E)
	     ((EQ (CAAR E) 'LAMBDA) (REDUCE1 (CONVERT E)))
	     ((EQ (CAR E) 'LAMBDA)
	      (LIST 'LAMBDA (CADR E) (REDUCE1 (CADDR E))))
	     (T (MAPCAR (FUNCTION REDUCE1) E)))) 

(DEFUN REDUCE2 (E) 
       (COND ((ATOM E) E)
	     ((EQ (CAAR E) 'LAMBDA)
	      (REDUCE2 (CONVERT (CONS (LIST 'LAMBDA
					    (CADAR E)
					    (REDUCE2 (CADDAR E)))
				      (CDR E)))))
	     ((EQ (CAR E) 'LAMBDA)
	      (LIST 'LAMBDA (CADR E) (REDUCE2 (CADDR E))))
	     (T (MAPCAR (FUNCTION REDUCE2) E)))) 

(DEFUN CONVERT (E) (NEWSUBLIS (PAIRUP (CADAR E) (CDR E)) (CADDAR E))) 

(DEFUN PAIRUP (U V) 
       (COND ((NULL U) NIL)
	     (T (CONS (CONS (CAR U) (CAR V))
		      (PAIRUP (CDR U) (CDR V)))))) 

(DEFUN NEWSUBLIS (P E) 
       (COND ((ATOM E)
	      ((LAMBDA (Z) (COND ((NULL Z) E) (T (CDR Z))))
	       (ASSOC E P)))
	     ((ISQUANT (CAR E))
	      (CONS (CAR E)
		    (NEWSUBLIS (APPEND P (NEWPAIRS (CADR E)))
			       (CDR E))))
	     (T (CONS (NEWSUBLIS P (CAR E)) (NEWSUBLIS P (CDR E)))))) 

(DEFUN ISQUANT (SYM) (MEMBER SYM '(ALL EXIST LAMBDA))) 

(DEFUN NEWPAIRS (U) 
       (COND ((NULL U) NIL)
	     (T (CONS (CONS (CAR U) (GENSYM)) (NEWPAIRS (CDR U)))))) 

(SETQ CAR '(LAMBDA (X Y) X)) 

(SETQ CDR '(LAMBDA (X Y) Y)) 

(SETQ IF '(LAMBDA (X Y Z) (X Y Z))) 

(DEFUN REDUCE3 (E) 
       (COND ((ATOM E) E)
	     ((EQ (CAAR E) 'LAMBDA) (REDUCE3 (CONVERT E)))
	     ((EQ (CAR E) 'LAMBDA)
	      (LIST 'LAMBDA (CADR E) (REDUCE3 (CADDR E))))
	     ((ATOM (CAR E)) (MAPCAR (FUNCTION REDUCE3) E))
	     (T (REDUCE3 (CONS (REDUCE3 (CAR E)) (CDR E)))))) 

(DEFUN REDUCE4 (E) 
       (COND ((ATOM E) E)
	     ((EQ (CAAR E) 'LAMBDA)
	      (REDUCE2 (CONVERT (CONS (LIST 'LAMBDA
					    (CADAR E)
					    (REDUCE2 (CADDAR E)))
				      (CDR E)))))
	     ((EQ (CAR E) 'LAMBDA)
	      (LIST 'LAMBDA (CADR E) (REDUCE4 (CADDR E))))
	     ((ATOM (CAR E)) (MAPCAR (FUNCTION REDUCE4) E))
	     (T (REDUCE4 (CONS (REDUCE4 (CAR E)) (CDR E))))))